Nuprl Lemma : compose_wf 13,42

ABC:Type, f:(BC), g:(AB). (f o g AC 
latex


Upfun 1, fun 1
Definitionsf o g, t  T, x:AB(x)

origin